% !TEX root = eventb-fac.tex


%\paragraph{Self-Adaptive Multiparty Sessions, In a Nutshell.} %\label{ss:dezani}
Here we  summarize the approach to session adaptation put forward in~\cite{CDV15j}. 
%The purpose of this summary is two-fold: on the one hand, it 
This 
enables us to illustrate the distinguishing features of a  recent approach to adaptation in the multiparty setting.
Also, it allows us to introduce some definitions and notions on which we will build upon in \S\,\ref{s:multi}.

The 
approach in~\cite{CDV15j} relies on %five technical ingredients, namely 
\emph{global types}, \emph{monitors}, \emph{processes}, \emph{networks}, and \emph{systems}.
Global types describe communications and explicit adaptation synchronizations; monitors, derived from global types, describe the protocol from the perspective of a single participant. Processes only specify communicating behavior; they are associated to monitors that regulate their communicating behavior and contain information on senders/receivers. 
Each protocol participant is then defined as a monitored process, a process tied with a monitor.
Networks are collections of monitored processes, together with constructs for starting new global protocols and queues for asynchronous communication. A system is the composition of a network with a \emph{global state}, an unspecified collection of data that may influence adaptation. The syntax of  global types in~\cite{CDV15j} 
%$\mathsf{G}, \mathsf{G}', \ldots$ 
includes directed communications and explicit adaptation signals:
%\[
%\mathsf{G} ::= \pt{p} \rightarrow \Pi :\{l_i(S_i).\mathsf{G}_i\}_{i\in I} \sepr 
%\pt{p} \rightarrow \Pi :\{\lambda_i\}_{i\in I} \sepr
%\mathsf{end}
%\] 
$$
\begin{array}{rll}
\mathsf{G} , \mathsf{G}'::= & \pt{p} \rightarrow \Pi :\{l_i(S_i).\mathsf{G}_i\}_{i\in I}  & \text{directed communication with labeled alternatives}\\ 
       \sep & \pt{p} \rightarrow \Pi :\{\lambda_i\}_{i\in I} \qquad & \text{adaptation flag} \\
  \sep & \mathsf{end} & \text{terminated protocol}
   \end{array}
$$
\noindent 
where 
$\pt{p}, \pt{q}, \ldots$ denote individual participants and $\Pi$ represents a set of participants. 
Also, 
$l_1, l_2, \ldots$ denote \emph{labels}, $S_1, S_2, \ldots$ denote carried types (e.g., $\mathtt{Bool}$, $\mathtt{Int}$)  and $\lambda_1, \lambda_2, \ldots$ denote \emph{adaptation flags}.
Thus, global types abstract sequences of broadcast-like communications from a single participant to a set of participants; such communications include usual labeled messages and also explicit adaptation signals.
%Recursion is absent. 
The set of \emph{monitors} is defined as follows:
\[
\mathsf{M} ::= \pt{p}?\{l_i(S_i).\mathsf{M}_i\}_{i\in I} \sepr 
			\Pi!\{l_i(S_i).\mathsf{M}_i\}_{i\in I} \sepr
			\pt{p}?\{\lambda_i\}_{i\in I} \sepr
			\Pi!\{\lambda_i\}_{i\in I} \sepr \mathsf{end}
\]
Formally, global types and monitors are related via a \emph{projection} function which establishes how a global type can be decomposed into monitors. Projection also determines valid global types: a global type is said to be \emph{well-formed} if (i)~its projections are defined for all participants, and if (ii)~exchanges of adaptation flags involve all participants declared in the global type. The syntax of processes is as follows:
%\[
\begin{eqnarray*}
 P  &::= & c?l(x).P \sepr c!l(e).P \sepr  c?l(\lambda, \mathtt{T}).P \sepr c!l(\lambda(F),\mathtt{T} ).P  
  \sepr \mathsf{op}.P \sepr \ifte{e}{P}{Q} \sepr  P + P \sepr \mu \rv{X}.P \sepr  \rv{X}  \sepr \nil
\end{eqnarray*}
%\]
Each process owns a unique \emph{channel}, denoted $c$ above. 
At runtime, channels specify a session channel and the identity of the current participant.
Most process constructs are standard; processes 
$\mathsf{op}.P$, 
$c?l(\lambda, \mathtt{T}).P$, and $c!l(\lambda(F),\mathtt{T} ).P$
deserve additional explanations. 
First, process $\mathsf{op}.P$ specifies an operation that modifies the global state; as such, it connects the behavior of communicating processes to future adaptation actions. Then, 
$c?l(\lambda, \mathtt{T}).P$
denotes a process which receives an adaptation flag $\lambda$ and has a continuation of type $\mathtt{T}$.
Finally, the process 
$c!l(\lambda(F),\mathtt{T} ).P$ 
is similar; it also specifies an \emph{adaptation function} $F$, which in combination with the global state will determine a new global type.

%In the approach of~\cite{CDV15j}, 
Given a monitor $\mathsf{M}$
and a process $P$, 
a monitored process is denoted $\monpro{\mathsf{M}}{P}$.
Adaptation actions  manifest at the level of networks; they are realized directly over monitors but indirectly over processes: the modification of 
the global type of the system results into a new set of monitors associated to processes; 
if a current process does not ``fit'' its new monitor, then it must be replaced with a different process,
obtained from a centralized collection of   pairs $(P, \mathtt{T})$, denoted $\mathcal{P}$, a parameter of the framework.
This  collection   is assumed to be complete, in the sense that all it contains processes for all conceivable monitors. Formally, the fit between processes and monitors is defined as an adequacy relation, denoted $\propto$, which uses subtyping to relate the type of processes and monitors. 

%We close  by describing the operational semantics of processes, networks, and systems. 
The semantics of processes is given in terms of a  labeled transition system (LTS) in which actions describe a session and the current participant. These actions are used to enforce the consistency between a process and its associated monitor, as formally captured by the semantics of networks. 
This semantics describes how each participant reacts to an adaptation request (i.e.,  a new global type) issued by another participant. Depending on whether or not the current process is adequate to the new monitor then the process implementation is kept or replaced, as described before. The 
semantics of systems specifies how a single participant communicates a new global type for the whole system. Indeed, as the selection of the new global type depends on the adaptation function $F$ and the global state, the new global type can only be described at the level of systems, rather than at the level of networks. This selection is communicated to participants using the shared queue, and locally handled at the level of networks, as just explained. Notice the new global type may determine a new set of participants, and so some of the current participants may be excluded as a result of adaptation. The new global type may also determine a new implementation for the participant invoking global reconfiguration; here again adequacy is used to determine whether a process reconfiguration is required or not.
%Correctness properties include subject reduction and progress.

\paragraph{Our Approach.}
Our previous example can be extended to the multyparty scenario by adding a new participant a \emph{shipper} to the conversation. The session protocol is  modified as follows: the buyer $\pt{b}$ asks for an item to the seller $\pt{s}$, who replies with its price. The buyer then confirms its order and pays it by sending to the seller her credit card number and to the shipper $\pt{p}$ her address. The seller finalizes the order by sending the name of the item to the shipper.  

Differently from above, we now have a protocol that globally describes the behavior of all participants:
\[
\gtype{G}::=\pt{b} \rightarrow \pt{s}: it(item). \pt{s} \rightarrow \pt{b} : price(int) . \pt{b}  \rightarrow \pt{s} : ok(bool) . \pt{b} \rightarrow \pt{s} : card(int) . \pt{b} \rightarrow \pt{p} : ad(string) . \pt{s} \rightarrow \pt{p}: itname(item)
\]
%where $p \rightarrow q : \lambda(S).G$ means that participant $p$ sends to $q$ a message of sort $S$ labelled $\lambda$.

As mentioned above, in the multiparty scenario, locations adopt a slightly different meaning. Each location is associated to only one participant in the conversation and contains a local collection   of typed processes $\Pool$ that represents possible programs to be run upon session establishment. 
The philosophy behind this choice is that a location may correspond to a ``computing entity'' possibly running distinct programs, e.g., a smartphone where a set of application are installed and can be executed depending on the need. 
Thus the three participants above can be implemented by the locations:
\[
\begin{array}{c}
 \text{Buyer:} ~~ \scomponent{\locf{loc_b}}{\Pool_\pt{b}; \que{\locf{loc}_\pt{b}}{\epsilon}}\quad
 \text{Seller:} ~~\scomponent{\locf{loc_s}}{\Pool_\pt{s}; \que{\locf{loc}_\pt{s}}{\epsilon}}\quad
 \text{Shipper:}~~ \scomponent{\locf{loc_{p}}}{\Pool_{\pt{p}}; \que{\locf{loc}_{\pt{p}}}{\epsilon}}
\end{array}
\]
where,
for each $\pt{q} \in \{\pt{b},\pt{s},\pt{p}\}$, 
 $\que{\locf{loc}_\pt{q}}{\epsilon}$ is an event queue that is used to signal the presence of an  adaption routine; it has the same behavior as in the binary case.
The collection $\Pool_\pt{q}$ contains an implementation of the local  protocol of each participant (which can be obtained projecting the global protocol into each participant). We therefore have the following processes:
\[
\begin{array}{l}
 P_\pt{b} ::= y!it(item).y?price(x).y!ok(true).y!card(number).y!ad(address)\\
 P_\pt{s} ::= y?it(x_1).(\ifte{ (x_1 =item1)}{y!price(1).y?ok(x_2).y?card(x_3).y!itname(x_1)\\\hspace{4.4cm}}
                    { y!price(2).y?ok(x_2).y?card(x_3).y!itname(x_1)} \\
 P_{\pt{p}} ::= y?ad(x_1).y?itname(x_2)           
\end{array}
\]

As in the binary case, in our proof of concept we define two kinds of adaptation, 
namely external and internal adaptation.
The form of external adaptation that 
we consider 
behaves quite similarly as the adaptation of binary processes; our mechanism for internal adaptation is meant to 
modify the current global protocol at runtime. Indeed, 
an internal adaptation routine is started by one of the participants who warns the others that a new protocol should be followed.
As an example in the buyer-seller-shipper scenario, we can imagine that  after having chosen an item, 
the buyer asks to the other participants to change the protocol, as she wishes to change the payment method from credit card to bank transfer. 
This adaptation routine will cause the buyer and the seller to change their implementations, while the shipper will remain unchanged. Moreover, a new participant (the bank \pt{k}) will be added to the conversation.
The new global protocol will then be:
\[
\gtype{G}'::= \pt{s} \rightarrow \pt{b} : iban(string). \pt{b} \rightarrow \pt{k} : iban(string) . \pt{b} \rightarrow \pt{p} : ad(string) . \pt{s} \rightarrow \pt{p}: itname(item)
\]
and the idea is that current communications are stopped, and the current active process is substituted with a another one that implements the new protocol. The semantics for networks would lead to the following adapted process:
\[
\begin{array}{l}
\restr{\kappa}{(
\scomponent{\locf{loc_b}}{y!card(number).y!ad(address) ;\Pool_\pt{b}; \que{\locf{loc}_\pt{b}}{\epsilon}} \para \\
\hspace{1cm}\scomponent{\locf{loc_\pt{s}}}{y?card(x).y!itname(x_1);\Pool_\pt{s}; \que{\locf{loc}_\pt{s}}{\epsilon}} \para 
 \scomponent{\locf{loc_{\pt{p}}}}{y?ad(x_1).y?itname(x_2); \Pool_{\pt{p}}; \que{\locf{loc}_{\pt{p}}}{\epsilon}} 
 )} \pired  \\
\restr{\kappa}{(
\scomponent{\locf{loc_\pt{b}}}{y?iban(x). y!iban(x).y!ad(address) ;\Pool_\pt{b}; \que{\locf{loc}_\pt{b}}{\epsilon}} \para 
\scomponent{\locf{loc_{\pt{k}}}}{y?iban(x) ;\Pool_{\pt{k}}; \que{loc_{\pt{k}}}{\epsilon}}\\
\hspace{1cm}\scomponent{\locf{loc_\pt{s}}}{y!iban(ibstr).y!itname(x_1);\Pool_\pt{s}; \que{\locf{loc}_\pt{s}}{\epsilon}} \para 
 \scomponent{\locf{loc_{\pt{p}}}}{y?ad(x_1).y?itname(x_2); \Pool_{\pt{p}}; \que{\locf{loc}_{\pt{p}}}{\epsilon}} 
 )}   
\end{array}
\]


